es:ES, e1, e2, b:E, Q:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
(e1 <loc b)
 b  e2 
 [e1,pred(b)]~([a,b].Q(a,b))+
 [b,e2]~([a,b].Q(a,b))+
 [e1,e2]~([a,b].Q(a,b))+ 

latex

Definitions	t  T, x:A. B(x), loc(e), Id, E, x(s1,s2), P  Q, x,y. t(x;y), [e1,e2]~([a,b].p(a;b))+, ES, Prop, (e <loc e'), e  e' , b, False, A, P & Q, P  Q, pred(e), 1of(t), P  Q, x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b)
Lemmas	es-pplus wf, es-pred wf, es-le-loc, es-loc-pred, es-locl-iff, subtype rel self, es-le wf, es-locl wf, event system wf, es-pstar-q-partition, es-E wf, Id wf, es-loc wf